package interfaces;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;


@Init ({"getRespuesta()!=null && getValoracion()<=5 && getValoracion()>=-5 && getTiempoEmpleado()>=0 && getTiempoEmpleado()<=Integer.MAX_VALUE "})
@Inv ({"getTiempoEmpleado()>=0"})

public interface IRespuesta {
	
	@Query
	public String getRespuesta();
	
	@Query
	public int getValoracion();
	
	@Query
	public int getTiempoEmpleado();
	
	@Query int getIdRespuesta();
	
	@Pre ({"nuevaValoracion>=-5 && nuevaValoracion<=5 #IllegalArgumentException"})
	@Pos ({"getValoracion() == nuevaValoracion && getRespuesta().equals(getRespuesta()@pre) && getTiempoEmpleado()==getTiempoEmpleado()@pre && getIdRespuesta() == getIdRespuesta()@Pre"})
	public void setValoracion(int nuevaValoracion);
	
	@Pre ({"nuevoIdRespuesta >= 0 && nuevoIdRespuesta <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos ({"getValoracion == getValoracion()@pre && getRespuesta().equals(getRespuesta()@pre) && getTiempoEmpleado()==getTiempoEmpleado()@pre && getIdRespuesta() == nuevoIdRespuesta"})
	public void setIdRespuesta(int nuevoIdRespuesta);
	
	@Pre({"nuevaRespuesta!=null #NullPointerException"})
	@Pos({"getRespuesta().equeals(nuevaRespuesta) && getTiempoEmpleado()==getTiempoEmpleado()@pre && getValoracion() == getValoracion()@pre && getIdRespuesta() == getIdRespuesta()@Pre"})
	public void setRespuesta(String nuevaRespuesta);
	
	@Pre({"tiempoNuevo>=0  && tiempoNuevo <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos({"getTiempoEmpleado()==tiempoNuevo && getRespuesta().equals(getRespuesta()@pre) && getValoracion()==getValoracion()@pre && getIdRespuesta() == getIdRespuesta()@Pre"})
	public void setTiempoEmpleado(int tiempoNuevo);
}
